pred(s(x)) → x
minus(x, 0) → x
minus(x, s(y)) → pred(minus(x, y))
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(0)) → 0
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
↳ QTRS
↳ DependencyPairsProof
pred(s(x)) → x
minus(x, 0) → x
minus(x, s(y)) → pred(minus(x, y))
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(0)) → 0
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
QUOT(s(x), s(y)) → QUOT(minus(x, y), s(y))
LOG(s(s(x))) → QUOT(x, s(s(0)))
LOG(s(s(x))) → LOG(s(quot(x, s(s(0)))))
MINUS(x, s(y)) → MINUS(x, y)
QUOT(s(x), s(y)) → MINUS(x, y)
MINUS(x, s(y)) → PRED(minus(x, y))
pred(s(x)) → x
minus(x, 0) → x
minus(x, s(y)) → pred(minus(x, y))
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(0)) → 0
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
QUOT(s(x), s(y)) → QUOT(minus(x, y), s(y))
LOG(s(s(x))) → QUOT(x, s(s(0)))
LOG(s(s(x))) → LOG(s(quot(x, s(s(0)))))
MINUS(x, s(y)) → MINUS(x, y)
QUOT(s(x), s(y)) → MINUS(x, y)
MINUS(x, s(y)) → PRED(minus(x, y))
pred(s(x)) → x
minus(x, 0) → x
minus(x, s(y)) → pred(minus(x, y))
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(0)) → 0
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
MINUS(x, s(y)) → MINUS(x, y)
pred(s(x)) → x
minus(x, 0) → x
minus(x, s(y)) → pred(minus(x, y))
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(0)) → 0
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MINUS(x, s(y)) → MINUS(x, y)
The value of delta used in the strict ordering is 4.
POL(MINUS(x1, x2)) = (4)x_2
POL(s(x1)) = 1 + (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
pred(s(x)) → x
minus(x, 0) → x
minus(x, s(y)) → pred(minus(x, y))
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(0)) → 0
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
QUOT(s(x), s(y)) → QUOT(minus(x, y), s(y))
pred(s(x)) → x
minus(x, 0) → x
minus(x, s(y)) → pred(minus(x, y))
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(0)) → 0
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
QUOT(s(x), s(y)) → QUOT(minus(x, y), s(y))
The value of delta used in the strict ordering is 1.
POL(minus(x1, x2)) = 1 + (9/4)x_1
POL(QUOT(x1, x2)) = (4)x_1
POL(pred(x1)) = x_1
POL(s(x1)) = 5/4 + (9/4)x_1
POL(0) = 0
pred(s(x)) → x
minus(x, 0) → x
minus(x, s(y)) → pred(minus(x, y))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
pred(s(x)) → x
minus(x, 0) → x
minus(x, s(y)) → pred(minus(x, y))
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(0)) → 0
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
LOG(s(s(x))) → LOG(s(quot(x, s(s(0)))))
pred(s(x)) → x
minus(x, 0) → x
minus(x, s(y)) → pred(minus(x, y))
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(0)) → 0
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
LOG(s(s(x))) → LOG(s(quot(x, s(s(0)))))
The value of delta used in the strict ordering is 117/16.
POL(LOG(x1)) = (13/4)x_1
POL(minus(x1, x2)) = x_1
POL(quot(x1, x2)) = 3/2 + (2)x_1
POL(pred(x1)) = (1/2)x_1
POL(s(x1)) = 5/2 + (9/4)x_1
POL(0) = 2
pred(s(x)) → x
minus(x, 0) → x
minus(x, s(y)) → pred(minus(x, y))
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
pred(s(x)) → x
minus(x, 0) → x
minus(x, s(y)) → pred(minus(x, y))
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(s(0)) → 0
log(s(s(x))) → s(log(s(quot(x, s(s(0))))))